FDL - Step of Proof: implies_functionality_wrt

Step of Proof: implies_functionality_wrt_implies

Inference at *
Iof proof for Lemma implies functionality wrt implies:

P1,P2,Q1,Q2:

. {P1

P2}

{Q1

Q2}

{(P1

Q1)

Q2}

by ((((((Unfold `guard` 0)

CollapseTHEN (GenUnivCD))

)

CollapseTHENM (HypBackchain))

)

CoCollapseTHEN ((Auto_aux (first_nat 1:n) ((first_nat 1:n),(first_nat 3:n)) (first_tok :t

C) inil_term)))

Definitions t T, {T}, P Q, , x:A. B(x), P Q

Lemmas rev implies wf

Definitions	t T, {T}, P Q, , x:A. B(x), P Q
Lemmas	rev implies wf